T:Type, L:(TProp) List, P:(TProp).
(x:T. Dec(P(x)))
 (QL. x:T. Dec(Q(x)))
 (QL. finite-type({x:T| Q(x) }))
 (x:T. P(x)  (QL.Q(x)))
 finite-type({x:T| P(x) }) 

latex

Definitions	t  T, x(s), x:A. B(x), P  Q, P  Q, x. t(x), P & Q, P  Q, xL. P(x), Prop, Dec(P), finite-type(T), (xL.P(x)), (x  l), l[i], x:A. B(x), ||as||, {i..j}, False, A, AB, i  j < k, ij, , upto(n), 1of(t), map(f;as), concat(ll), A & B, {T}, SQType(T), True, T
Lemmas	member upto, le wf, member-concat, exists functionality wrt iff, and functionality wrt iff, member map, concat wf, map wf, pi1 wf, upto wf, non neg length, l member wf, int seg wf, length wf1, select wf, select member, l exists wf, finite-type wf, l all wf, decidable wf, finite-decidable-set